type name;
type ref;
const unique null : ref;
type real;
type elements;
type struct;
type exposeVersionType;
var $Heap : <x>[ref, name]x where IsHeap($Heap);
function IsHeap(h : <x>[ref, name]x) returns ($$unnamed~a : bool);
const $allocated : name;
const $elements : name;
const $inv : name;
const $localinv : name;
const $exposeVersion : name;
axiom (DeclType($exposeVersion) == System.Object);
const $sharingMode : name;
const $SharingMode_Unshared : name;
const $SharingMode_LockProtected : name;
const $ownerRef : name;
const $ownerFrame : name;
const $PeerGroupPlaceholder : name;
function ClassRepr(class : name) returns ($$unnamed~b : ref);
axiom (forall c0 : name, c1 : name :: {ClassRepr(c0), ClassRepr(c1)} ((c0 != c1) ==> (ClassRepr(c0) != ClassRepr(c1))));
axiom (forall T : name :: !($typeof(ClassRepr(T)) <: System.Object));
axiom (forall T : name :: (ClassRepr(T) != null));
axiom (forall T : name, h : <x>[ref, name]x :: {h[ClassRepr(T), $ownerFrame]} (IsHeap(h) ==> (h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder)));
function IsDirectlyModifiableField(f : name) returns ($$unnamed~c : bool);
axiom !IsDirectlyModifiableField($allocated);
axiom IsDirectlyModifiableField($elements);
axiom !IsDirectlyModifiableField($inv);
axiom !IsDirectlyModifiableField($localinv);
axiom !IsDirectlyModifiableField($ownerRef);
axiom !IsDirectlyModifiableField($ownerFrame);
axiom !IsDirectlyModifiableField($exposeVersion);
function IsStaticField(f : name) returns ($$unnamed~d : bool);
axiom !IsStaticField($allocated);
axiom !IsStaticField($elements);
axiom !IsStaticField($inv);
axiom !IsStaticField($localinv);
axiom !IsStaticField($exposeVersion);
function ValueArrayGet<any>($$unnamed~f : elements, $$unnamed~e : int) returns ($$unnamed~g : any);
function ValueArraySet<any>($$unnamed~j : elements, $$unnamed~i : int, $$unnamed~h : any) returns ($$unnamed~k : elements);
function RefArrayGet($$unnamed~m : elements, $$unnamed~l : int) returns ($$unnamed~n : ref);
function RefArraySet($$unnamed~q : elements, $$unnamed~p : int, $$unnamed~o : ref) returns ($$unnamed~r : elements);
axiom (forall<any> A : elements, i : int, x : any :: (ValueArrayGet(ValueArraySet(A, i, x), i) == x));
axiom (forall<any> A : elements, i : int, j : int, x : any :: ((i != j) ==> (ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j))));
axiom (forall A : elements, i : int, x : ref :: (RefArrayGet(RefArraySet(A, i, x), i) == x));
axiom (forall A : elements, i : int, j : int, x : ref :: ((i != j) ==> (RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j))));
function ArrayIndex(arr : ref, dim : int, indexAtDim : int, remainingIndexContribution : int) returns ($$unnamed~s : int);
axiom (forall a : ref, d : int, x : int, y : int, x' : int, y' : int :: {ArrayIndex(a, d, x, y), ArrayIndex(a, d, x', y')} ((ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y')) ==> ((x == x') && (y == y'))));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: RefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: RefArray(T, r))) ==> $Is(RefArrayGet(heap[a, $elements], i), T)));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: NonNullRefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: NonNullRefArray(T, r))) ==> $IsNotNull(RefArrayGet(heap[a, $elements], i), T)));
function $Rank($$unnamed~t : ref) returns ($$unnamed~u : int);
axiom (forall a : ref :: (1 <= $Rank(a)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: RefArray(T, r))} (((a != null) && ($typeof(a) <: RefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: NonNullRefArray(T, r))} (((a != null) && ($typeof(a) <: NonNullRefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: ValueArray(T, r))} (((a != null) && ($typeof(a) <: ValueArray(T, r))) ==> ($Rank(a) == r)));
function $Length($$unnamed~v : ref) returns ($$unnamed~w : int);
axiom (forall a : ref :: {$Length(a)} (0 <= $Length(a)));
function $DimLength($$unnamed~y : ref, $$unnamed~x : int) returns ($$unnamed~z : int);
axiom (forall a : ref, i : int :: (0 <= $DimLength(a, i)));
axiom (forall a : ref :: {$DimLength(a, 0)} (($Rank(a) == 1) ==> ($DimLength(a, 0) == $Length(a))));
function $LBound($$unnamed~ab : ref, $$unnamed~aa : int) returns ($$unnamed~ac : int);
function $UBound($$unnamed~ae : ref, $$unnamed~ad : int) returns ($$unnamed~af : int);
axiom (forall a : ref, i : int :: {$LBound(a, i)} ($LBound(a, i) == 0));
axiom (forall a : ref, i : int :: {$UBound(a, i)} ($UBound(a, i) == ($DimLength(a, i) - 1)));
const $ArrayCategoryValue : name;
const $ArrayCategoryRef : name;
const $ArrayCategoryNonNullRef : name;
function $ArrayCategory(arrayType : name) returns (arrayCategory : name);
axiom (forall T : name, ET : name, r : int :: {(T <: ValueArray(ET, r))} ((T <: ValueArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryValue)));
axiom (forall T : name, ET : name, r : int :: {(T <: RefArray(ET, r))} ((T <: RefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryRef)));
axiom (forall T : name, ET : name, r : int :: {(T <: NonNullRefArray(ET, r))} ((T <: NonNullRefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryNonNullRef)));
const System.Array : name;
axiom (System.Array <: System.Object);
function $ElementType($$unnamed~ag : name) returns ($$unnamed~ah : name);
function ValueArray(elementType : name, rank : int) returns ($$unnamed~ai : name);
axiom (forall T : name, r : int :: {ValueArray(T, r)} (ValueArray(T, r) <: System.Array));
function RefArray(elementType : name, rank : int) returns ($$unnamed~aj : name);
axiom (forall T : name, r : int :: {RefArray(T, r)} (RefArray(T, r) <: System.Array));
function NonNullRefArray(elementType : name, rank : int) returns ($$unnamed~ak : name);
axiom (forall T : name, r : int :: {NonNullRefArray(T, r)} (NonNullRefArray(T, r) <: System.Array));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (RefArray(U, r) <: RefArray(T, r))));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (NonNullRefArray(U, r) <: NonNullRefArray(T, r))));
axiom (forall A : name, r : int :: ($ElementType(ValueArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(RefArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(NonNullRefArray(A, r)) == A));
axiom (forall A : name, r : int, T : name :: {(T <: RefArray(A, r))} ((T <: RefArray(A, r)) ==> ((T == RefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: NonNullRefArray(A, r))} ((T <: NonNullRefArray(A, r)) ==> ((T == NonNullRefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: ValueArray(A, r))} ((T <: ValueArray(A, r)) ==> (T == ValueArray(A, r))));
axiom (forall A : name, r : int, T : name :: ((RefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == RefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((NonNullRefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == NonNullRefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((ValueArray(A, r) <: T) ==> ((System.Array <: T) || (T == ValueArray(A, r)))));
function $ArrayPtr(elementType : name) returns ($$unnamed~al : name);
function $StructGet<any>($$unnamed~an : struct, $$unnamed~am : name) returns ($$unnamed~ao : any);
function $StructSet<any>($$unnamed~ar : struct, $$unnamed~aq : name, $$unnamed~ap : any) returns ($$unnamed~as : struct);
axiom (forall<any> s : struct, f : name, x : any :: ($StructGet($StructSet(s, f, x), f) == x));
axiom (forall<any> s : struct, f : name, f' : name, x : any :: ((f != f') ==> ($StructGet($StructSet(s, f, x), f') == $StructGet(s, f'))));
function ZeroInit(s : struct, typ : name) returns ($$unnamed~at : bool);
function $typeof($$unnamed~au : ref) returns ($$unnamed~av : name);
function $BaseClass(sub : name) returns (base : name);
function AsDirectSubClass(sub : name, base : name) returns (sub' : name);
function OneClassDown(sub : name, base : name) returns (directSub : name);
axiom (forall A : name, B : name, C : name :: {(C <: AsDirectSubClass(B, A))} ((C <: AsDirectSubClass(B, A)) ==> (OneClassDown(C, A) == B)));
function $IsValueType($$unnamed~aw : name) returns ($$unnamed~ax : bool);
axiom (forall T : name :: ($IsValueType(T) ==> ((forall U : name :: ((T <: U) ==> (T == U))) && (forall U : name :: ((U <: T) ==> (T == U))))));
const System.Object : name;
function $IsTokenForType($$unnamed~az : struct, $$unnamed~ay : name) returns ($$unnamed~ba : bool);
function TypeObject($$unnamed~bb : name) returns ($$unnamed~bc : ref);
const System.Type : name;
axiom (System.Type <: System.Object);
axiom (forall T : name :: {TypeObject(T)} $IsNotNull(TypeObject(T), System.Type));
function TypeName($$unnamed~bd : ref) returns ($$unnamed~be : name);
axiom (forall T : name :: {TypeObject(T)} (TypeName(TypeObject(T)) == T));
function $Is($$unnamed~bg : ref, $$unnamed~bf : name) returns ($$unnamed~bh : bool);
axiom (forall o : ref, T : name :: {$Is(o, T)} ($Is(o, T) <==> ((o == null) || ($typeof(o) <: T))));
function $IsNotNull($$unnamed~bj : ref, $$unnamed~bi : name) returns ($$unnamed~bk : bool);
axiom (forall o : ref, T : name :: {$IsNotNull(o, T)} ($IsNotNull(o, T) <==> ((o != null) && $Is(o, T))));
function $As($$unnamed~bm : ref, $$unnamed~bl : name) returns ($$unnamed~bn : ref);
axiom (forall o : ref, T : name :: ($Is(o, T) ==> ($As(o, T) == o)));
axiom (forall o : ref, T : name :: (!$Is(o, T) ==> ($As(o, T) == null)));
axiom (forall h : <x>[ref, name]x, o : ref :: {($typeof(o) <: System.Array), h[o, $inv]} (((IsHeap(h) && (o != null)) && ($typeof(o) <: System.Array)) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
function IsAllocated<any>(h : <x>[ref, name]x, o : any) returns ($$unnamed~bo : bool);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {IsAllocated(h, h[o, f])} ((IsHeap(h) && h[o, $allocated]) ==> IsAllocated(h, h[o, f])));
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[h[o, f], $allocated]} ((IsHeap(h) && h[o, $allocated]) ==> h[h[o, f], $allocated]));
axiom (forall h : <x>[ref, name]x, s : struct, f : name :: {IsAllocated(h, $StructGet(s, f))} (IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, RefArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, ValueArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, o : ref :: {h[o, $allocated]} (IsAllocated(h, o) ==> h[o, $allocated]));
axiom (forall h : <x>[ref, name]x, c : name :: {h[ClassRepr(c), $allocated]} (IsHeap(h) ==> h[ClassRepr(c), $allocated]));
const $BeingConstructed : ref;
const $NonNullFieldsAreInitialized : name;
function DeclType(field : name) returns (class : name);
function AsNonNullRefField(field : name, T : name) returns (f : name);
function AsRefField(field : name, T : name) returns (f : name);
function AsRangeField(field : name, T : name) returns (f : name);
axiom (forall f : name, T : name :: {AsNonNullRefField(f, T)} ((AsNonNullRefField(f, T) == f) ==> (AsRefField(f, T) == f)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRefField(f, T)]} (IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsNonNullRefField(f, T)]} (((IsHeap(h) && (o != null)) && ((o != $BeingConstructed) || (h[$BeingConstructed, $NonNullFieldsAreInitialized] == true))) ==> (h[o, AsNonNullRefField(f, T)] != null)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRangeField(f, T)]} (IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)));
function $IsMemberlessType($$unnamed~bp : name) returns ($$unnamed~bq : bool);
axiom (forall o : ref :: {$IsMemberlessType($typeof(o))} !$IsMemberlessType($typeof(o)));
function $IsImmutable(T : name) returns ($$unnamed~br : bool);
axiom !$IsImmutable(System.Object);
function $AsImmutable(T : name) returns (theType : name);
function $AsMutable(T : name) returns (theType : name);
axiom (forall T : name, U : name :: {(U <: $AsImmutable(T))} ((U <: $AsImmutable(T)) ==> ($IsImmutable(U) && ($AsImmutable(U) == U))));
axiom (forall T : name, U : name :: {(U <: $AsMutable(T))} ((U <: $AsMutable(T)) ==> (!$IsImmutable(U) && ($AsMutable(U) == U))));
function AsOwner(string : ref, owner : ref) returns (theString : ref);
axiom (forall o : ref, T : name :: {($typeof(o) <: $AsImmutable(T))} ((((o != null) && (o != $BeingConstructed)) && ($typeof(o) <: $AsImmutable(T))) ==> (forall h : <x>[ref, name]x :: {IsHeap(h)} (IsHeap(h) ==> (((((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o))) && (h[o, $ownerFrame] == $PeerGroupPlaceholder)) && (AsOwner(o, h[o, $ownerRef]) == o)) && (forall t : ref :: {AsOwner(o, h[t, $ownerRef])} ((AsOwner(o, h[t, $ownerRef]) == o) ==> ((t == o) || (h[t, $ownerFrame] != $PeerGroupPlaceholder)))))))));
const System.String : name;
function $StringLength($$unnamed~bs : ref) returns ($$unnamed~bt : int);
axiom (forall s : ref :: {$StringLength(s)} (0 <= $StringLength(s)));
function AsRepField(f : name, declaringType : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRepField(f, T)]} ((IsHeap(h) && (h[o, AsRepField(f, T)] != null)) ==> ((h[h[o, AsRepField(f, T)], $ownerRef] == o) && (h[h[o, AsRepField(f, T)], $ownerFrame] == T))));
function AsPeerField(f : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[o, AsPeerField(f)]} ((IsHeap(h) && (h[o, AsPeerField(f)] != null)) ==> ((h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef]) && (h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]))));
axiom (forall h : <x>[ref, name]x, o : ref :: {(h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])} ((((IsHeap(h) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
procedure $SetOwner(o : ref, ow : ref, fr : name);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[o, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[o, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == ow) && ($Heap[p, $ownerFrame] == fr))));
  

procedure $UpdateOwnersForRep(o : ref, T : name, e : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[e, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((e == null) ==> ($Heap == old($Heap)));
  ensures ((e != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[e, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == o) && ($Heap[p, $ownerFrame] == T)))));
  

procedure $UpdateOwnersForPeer(c : ref, d : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} ((((F != $ownerRef) && (F != $ownerFrame)) || old(((($Heap[p, $ownerRef] != $Heap[c, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[c, $ownerFrame])) && (($Heap[p, $ownerRef] != $Heap[d, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]))))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((d == null) ==> ($Heap == old($Heap)));
  ensures ((d != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} (((old(($Heap[p, $ownerRef] == $Heap[c, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[c, $ownerFrame]))) || (old(($Heap[p, $ownerRef] == $Heap[d, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[d, $ownerFrame])))) ==> ((((old($Heap)[d, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[c, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame])) || (((old($Heap)[d, $ownerFrame] != $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[d, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[d, $ownerFrame]))))));
  

const $FirstConsistentOwner : name;
function $AsPureObject($$unnamed~bu : ref) returns ($$unnamed~bv : ref);
function ##FieldDependsOnFCO<any>(o : ref, f : name, ev : exposeVersionType) returns (value : any);
axiom (forall o : ref, f : name, h : <x>[ref, name]x :: {h[$AsPureObject(o), f]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion]))));
axiom (forall o : ref, h : <x>[ref, name]x :: {h[o, $FirstConsistentOwner]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (((h[o, $FirstConsistentOwner] != null) && (h[h[o, $FirstConsistentOwner], $allocated] == true)) && (((h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder) || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame])) || (h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))))));
function Box<any>($$unnamed~bx : any, $$unnamed~bw : ref) returns ($$unnamed~by : ref);
function Unbox<any>($$unnamed~bz : ref) returns ($$unnamed~ca : any);
axiom (forall<any> x : any, p : ref :: {Unbox(Box(x, p))} (Unbox(Box(x, p)) == x));
function UnboxedType($$unnamed~cb : ref) returns ($$unnamed~cc : name);
axiom (forall p : ref :: {$IsValueType(UnboxedType(p))} ($IsValueType(UnboxedType(p)) ==> (forall<any> heap : <x>[ref, name]x, x : any :: {heap[Box(x, p), $inv]} (IsHeap(heap) ==> ((heap[Box(x, p), $inv] == $typeof(Box(x, p))) && (heap[Box(x, p), $localinv] == $typeof(Box(x, p))))))));
axiom (forall<any> x : any, p : ref :: {(UnboxedType(Box(x, p)) <: System.Object)} (((UnboxedType(Box(x, p)) <: System.Object) && (Box(x, p) == p)) ==> (x == p)));
function BoxTester(p : ref, typ : name) returns ($$unnamed~cd : ref);
axiom (forall p : ref, typ : name :: {BoxTester(p, typ)} ((UnboxedType(p) == typ) <==> (BoxTester(p, typ) != null)));
const System.SByte : name;
axiom $IsValueType(System.SByte);
const System.Byte : name;
axiom $IsValueType(System.Byte);
const System.Int16 : name;
axiom $IsValueType(System.Int16);
const System.UInt16 : name;
axiom $IsValueType(System.UInt16);
const System.Int32 : name;
axiom $IsValueType(System.Int32);
const System.UInt32 : name;
axiom $IsValueType(System.UInt32);
const System.Int64 : name;
axiom $IsValueType(System.Int64);
const System.UInt64 : name;
axiom $IsValueType(System.UInt64);
const System.Char : name;
axiom $IsValueType(System.Char);
const int#m2147483648 : int;
const int#2147483647 : int;
const int#4294967295 : int;
const int#m9223372036854775808 : int;
const int#9223372036854775807 : int;
const int#18446744073709551615 : int;
axiom (int#m9223372036854775808 < int#m2147483648);
axiom (int#m2147483648 < (0 - 100000));
axiom (100000 < int#2147483647);
axiom (int#2147483647 < int#4294967295);
axiom (int#4294967295 < int#9223372036854775807);
axiom (int#9223372036854775807 < int#18446744073709551615);
function InRange(i : int, T : name) returns ($$unnamed~ce : bool);
axiom (forall i : int :: (InRange(i, System.SByte) <==> (((0 - 128) <= i) && (i < 128))));
axiom (forall i : int :: (InRange(i, System.Byte) <==> ((0 <= i) && (i < 256))));
axiom (forall i : int :: (InRange(i, System.Int16) <==> (((0 - 32768) <= i) && (i < 32768))));
axiom (forall i : int :: (InRange(i, System.UInt16) <==> ((0 <= i) && (i < 65536))));
axiom (forall i : int :: (InRange(i, System.Int32) <==> ((int#m2147483648 <= i) && (i <= int#2147483647))));
axiom (forall i : int :: (InRange(i, System.UInt32) <==> ((0 <= i) && (i <= int#4294967295))));
axiom (forall i : int :: (InRange(i, System.Int64) <==> ((int#m9223372036854775808 <= i) && (i <= int#9223372036854775807))));
axiom (forall i : int :: (InRange(i, System.UInt64) <==> ((0 <= i) && (i <= int#18446744073709551615))));
axiom (forall i : int :: (InRange(i, System.Char) <==> ((0 <= i) && (i < 65536))));
function $IntToInt(val : int, fromType : name, toType : name) returns ($$unnamed~cf : int);
function $IntToReal($$unnamed~cg : int, fromType : name, toType : name) returns ($$unnamed~ch : real);
function $RealToInt($$unnamed~ci : real, fromType : name, toType : name) returns ($$unnamed~cj : int);
function $RealToReal(val : real, fromType : name, toType : name) returns ($$unnamed~ck : real);
function $SizeIs($$unnamed~cm : name, $$unnamed~cl : int) returns ($$unnamed~cn : bool);
function $IfThenElse<any>($$unnamed~cq : bool, $$unnamed~cp : any, $$unnamed~co : any) returns ($$unnamed~cr : any);
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (b ==> ($IfThenElse(b, x, y) == x)));
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (!b ==> ($IfThenElse(b, x, y) == y)));
function #neg($$unnamed~cs : int) returns ($$unnamed~ct : int);
function #and($$unnamed~cv : int, $$unnamed~cu : int) returns ($$unnamed~cw : int);
function #or($$unnamed~cy : int, $$unnamed~cx : int) returns ($$unnamed~cz : int);
function #xor($$unnamed~db : int, $$unnamed~da : int) returns ($$unnamed~dc : int);
function #shl($$unnamed~de : int, $$unnamed~dd : int) returns ($$unnamed~df : int);
function #shr($$unnamed~dh : int, $$unnamed~dg : int) returns ($$unnamed~di : int);
function #rneg($$unnamed~dj : real) returns ($$unnamed~dk : real);
function #radd($$unnamed~dm : real, $$unnamed~dl : real) returns ($$unnamed~dn : real);
function #rsub($$unnamed~dp : real, $$unnamed~do : real) returns ($$unnamed~dq : real);
function #rmul($$unnamed~ds : real, $$unnamed~dr : real) returns ($$unnamed~dt : real);
function #rdiv($$unnamed~dv : real, $$unnamed~du : real) returns ($$unnamed~dw : real);
function #rmod($$unnamed~dy : real, $$unnamed~dx : real) returns ($$unnamed~dz : real);
function #rLess($$unnamed~eb : real, $$unnamed~ea : real) returns ($$unnamed~ec : bool);
function #rAtmost($$unnamed~ee : real, $$unnamed~ed : real) returns ($$unnamed~ef : bool);
function #rEq($$unnamed~eh : real, $$unnamed~eg : real) returns ($$unnamed~ei : bool);
function #rNeq($$unnamed~ek : real, $$unnamed~ej : real) returns ($$unnamed~el : bool);
function #rAtleast($$unnamed~en : real, $$unnamed~em : real) returns ($$unnamed~eo : bool);
function #rGreater($$unnamed~eq : real, $$unnamed~ep : real) returns ($$unnamed~er : bool);
axiom (forall x : int, y : int :: {(x % y)} {(x / y)} ((x % y) == (x - ((x / y) * y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (0 < y)) ==> ((0 <= (x % y)) && ((x % y) < y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (y < 0)) ==> ((0 <= (x % y)) && ((x % y) < (0 - y)))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (0 < y)) ==> (((0 - y) < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (y < 0)) ==> ((y < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {((x + y) % y)} (((0 <= x) && (0 <= y)) ==> (((x + y) % y) == (x % y))));
axiom (forall x : int, y : int :: {((y + x) % y)} (((0 <= x) && (0 <= y)) ==> (((y + x) % y) == (x % y))));
axiom (forall x : int, y : int :: {((x - y) % y)} (((0 <= (x - y)) && (0 <= y)) ==> (((x - y) % y) == (x % y))));
axiom (forall a : int, b : int, d : int :: {(a % d), (b % d)} ((((2 <= d) && ((a % d) == (b % d))) && (a < b)) ==> ((a + d) <= b)));
axiom (forall x : int, y : int :: {#and(x, y)} (((0 <= x) || (0 <= y)) ==> (0 <= #and(x, y))));
axiom (forall x : int, y : int :: {#or(x, y)} (((0 <= x) && (0 <= y)) ==> ((0 <= #or(x, y)) && (#or(x, y) <= (x + y)))));
axiom (forall i : int :: {#shl(i, 0)} (#shl(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shl(i, (j + 1)) == (#shl(i, j) * 2))));
axiom (forall i : int :: {#shr(i, 0)} (#shr(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shr(i, (j + 1)) == (#shr(i, j) / 2))));
function #System.String.IsInterned$System.String$notnull($$unnamed~es : ref) returns ($$unnamed~et : ref);
function #System.String.Equals$System.String($$unnamed~ev : ref, $$unnamed~eu : ref) returns ($$unnamed~ew : bool);
function #System.String.Equals$System.String$System.String($$unnamed~ey : ref, $$unnamed~ex : ref) returns ($$unnamed~ez : bool);
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String(a, b)} (#System.String.Equals$System.String(a, b) == #System.String.Equals$System.String$System.String(a, b)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} (#System.String.Equals$System.String$System.String(a, b) == #System.String.Equals$System.String$System.String(b, a)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} ((((a != null) && (b != null)) && #System.String.Equals$System.String$System.String(a, b)) ==> (#System.String.IsInterned$System.String$notnull(a) == #System.String.IsInterned$System.String$notnull(b))));
const $UnknownRef : ref;
const Person.spouse : name;
const Person.possn : name;
const System.Collections.IEnumerable : name;
const Possession : name;
const System.IComparable : name;
const System.Runtime.InteropServices._MemberInfo : name;
const System.Reflection.IReflect : name;
const System.Runtime.InteropServices._Exception : name;
const System.Runtime.InteropServices._Type : name;
const Microsoft.Contracts.ObjectInvariantException : name;
const System.IEquatable`1...System.String : name;
const Microsoft.Contracts.GuardException : name;
const System.Reflection.ICustomAttributeProvider : name;
const System.Collections.Generic.IEnumerable`1...System.Char : name;
const System.IComparable`1...System.String : name;
const System.Runtime.Serialization.ISerializable : name;
const Person : name;
const Microsoft.Contracts.ICheckedException : name;
const System.ICloneable : name;
const System.Boolean : name;
const System.Exception : name;
const System.Reflection.MemberInfo : name;
const System.IConvertible : name;
axiom !IsStaticField(Person.spouse);
axiom IsDirectlyModifiableField(Person.spouse);
axiom (AsPeerField(Person.spouse) == Person.spouse);
axiom (DeclType(Person.spouse) == Person);
axiom (AsRefField(Person.spouse, Person) == Person.spouse);
axiom !IsStaticField(Person.possn);
axiom IsDirectlyModifiableField(Person.possn);
axiom (AsRepField(Person.possn, Person) == Person.possn);
axiom (DeclType(Person.possn) == Person);
axiom (AsRefField(Person.possn, Possession) == Person.possn);
axiom (Person <: Person);
axiom ($BaseClass(Person) == System.Object);
axiom ((Person <: $BaseClass(Person)) && (AsDirectSubClass(Person, $BaseClass(Person)) == Person));
axiom (!$IsImmutable(Person) && ($AsMutable(Person) == Person));
axiom (forall $U : name :: {($U <: Person)} (($U <: Person) ==> ($U == Person)));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: Person)} (((IsHeap($h) && ($h[$oi, $inv] <: Person)) && ($h[$oi, $localinv] != System.Object)) ==> (($h[$oi, Person.spouse] != null) ==> ($h[$h[$oi, Person.spouse], Person.spouse] == $oi))));
axiom (forall $U : name :: {($U <: System.Boolean)} (($U <: System.Boolean) ==> ($U == System.Boolean)));
procedure Person.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  var local0 : bool where true;
  var stack50000o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, Person); goto $$entry~b;
  $$entry~b: assume ($Heap[this, $allocated] == true); goto $$entry~a;
  $$entry~a: throwException := throwException$in; goto block1700;
  block1700: goto block1717;
  block1717: assert (this != null); goto $$block1717~b;
  $$block1717~b: stack0o := $Heap[this, Person.spouse]; goto $$block1717~a;
  $$block1717~a: stack1o := null; goto true1717to1802, false1717to1734;
  true1717to1802: assume (stack0o == stack1o); goto block1802;
  false1717to1734: assume (stack0o != stack1o); goto block1734;
  block1802: stack0b := true; goto block1819;
  block1734: assert (this != null); goto $$block1734~c;
  $$block1734~c: stack0o := $Heap[this, Person.spouse]; goto $$block1734~b;
  $$block1734~b: assert (stack0o != null); goto $$block1734~a;
  $$block1734~a: stack0o := $Heap[stack0o, Person.spouse]; goto true1734to1768, false1734to1751;
  true1734to1768: assume (stack0o == this); goto block1768;
  false1734to1751: assume (stack0o != this); goto block1751;
  block1768: stack0b := true; goto block1785;
  block1751: stack0b := false; goto block1785;
  block1819: goto true1819to1921, false1819to1836;
  true1819to1921: assume stack0b; goto block1921;
  false1819to1836: assume !stack0b; goto block1836;
  block1921: local0 := true; goto block1938;
  block1836: stack0b := throwException; goto true1836to1887, false1836to1853;
  block1785: goto block1819;
  true1836to1887: assume !stack0b; goto block1887;
  false1836to1853: assume stack0b; goto block1853;
  block1887: local0 := false; goto block1938;
  block1853: assume false; goto $$block1853~i;
  $$block1853~i: havoc stack50000o; goto $$block1853~h;
  $$block1853~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block1853~g;
  $$block1853~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block1853~f;
  $$block1853~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block1853~e;
  $$block1853~e: assert (stack50000o != null); goto $$block1853~d;
  $$block1853~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block1853~c;
  $$block1853~c: stack0o := stack50000o; goto $$block1853~b;
  $$block1853~b: assert (stack0o != null); goto $$block1853~a;
  $$block1853~a: assume false; return;
  block1938: SS$Display.Return.Local := local0; goto $$block1938~b;
  $$block1938~b: stack0b := local0; goto $$block1938~a;
  $$block1938~a: $result := stack0b; return;
  
}

axiom (Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException);
axiom (Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException);
axiom (System.Exception <: System.Exception);
axiom ($BaseClass(System.Exception) == System.Object);
axiom ((System.Exception <: $BaseClass(System.Exception)) && (AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception));
axiom (!$IsImmutable(System.Exception) && ($AsMutable(System.Exception) == System.Exception));
axiom (System.Runtime.Serialization.ISerializable <: System.Object);
axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable);
axiom (System.Exception <: System.Runtime.Serialization.ISerializable);
axiom (System.Runtime.InteropServices._Exception <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Exception);
axiom (System.Exception <: System.Runtime.InteropServices._Exception);
axiom ($BaseClass(Microsoft.Contracts.GuardException) == System.Exception);
axiom ((Microsoft.Contracts.GuardException <: $BaseClass(Microsoft.Contracts.GuardException)) && (AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException));
axiom (!$IsImmutable(Microsoft.Contracts.GuardException) && ($AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException));
axiom ($BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException);
axiom ((Microsoft.Contracts.ObjectInvariantException <: $BaseClass(Microsoft.Contracts.ObjectInvariantException)) && (AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException));
axiom (!$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && ($AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException));
procedure Microsoft.Contracts.ObjectInvariantException..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Microsoft.Contracts.ObjectInvariantException <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure Person.Marry$Person$notnull(this : ref, p$in : ref where $IsNotNull(p$in, Person));
  requires ($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[p$in, $allocated] == true);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (p$in != this);
  requires ($Heap[this, Person.spouse] == null);
  requires ($Heap[p$in, Person.spouse] == null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[p$in, $ownerRef], $inv] <: $Heap[p$in, $ownerFrame])) || ($Heap[$Heap[p$in, $ownerRef], $localinv] == $BaseClass($Heap[p$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[p$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[p$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[p$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[p$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[p$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[p$in, $ownerFrame]))))) && old(((($o != this) || ($f != Person.spouse)) && (($o != p$in) || ($f != Person.spouse))))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.Marry$Person$notnull(this : ref, p$in : ref) {
  var p : ref where $IsNotNull(p, Person);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~d;
  $$entry~d: assume ($Heap[this, $allocated] == true); goto $$entry~c;
  $$entry~c: p := p$in; goto block3298;
  block3298: goto block3655;
  block3655: temp0 := this; goto $$block3655~g;
  $$block3655~g: assert (temp0 != null); goto $$block3655~f;
  $$block3655~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block3655~e;
  $$block3655~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block3655~d;
  $$block3655~d: havoc temp1; goto $$block3655~c;
  $$block3655~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block3655~b;
  $$block3655~b: assume IsHeap($Heap); goto $$block3655~a;
  $$block3655~a: local2 := null; goto block3672;
  block3672: temp2 := p; goto $$block3672~g;
  $$block3672~g: assert (temp2 != null); goto $$block3672~f;
  $$block3672~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Person)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block3672~e;
  $$block3672~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block3672~d;
  $$block3672~d: havoc temp3; goto $$block3672~c;
  $$block3672~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block3672~b;
  $$block3672~b: assume IsHeap($Heap); goto $$block3672~a;
  $$block3672~a: local4 := null; goto block3689;
  block3689: assert (this != null); goto $$block3689~m;
  $$block3689~m: assert (!($Heap[this, $inv] <: Person) || ($Heap[this, $localinv] == System.Object)); goto $$block3689~l;
  $$block3689~l: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == this)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block3689~k;
  $$block3689~k: assert (((((p == null) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))))) || ((!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerRef] == $Heap[p, $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[p, $ownerFrame]))); goto $$block3689~j;
  $$block3689~j: $Heap := $Heap[this, Person.spouse := p]; goto $$block3689~i;
  $$block3689~i: call $UpdateOwnersForPeer(this, p); goto $$block3689~h;
  $$block3689~h: assume IsHeap($Heap); goto $$block3689~g;
  $$block3689~g: assert (p != null); goto $$block3689~f;
  $$block3689~f: assert (!($Heap[p, $inv] <: Person) || ($Heap[p, $localinv] == System.Object)); goto $$block3689~e;
  $$block3689~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == p)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block3689~d;
  $$block3689~d: assert (((((this == null) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[p, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block3689~c;
  $$block3689~c: $Heap := $Heap[p, Person.spouse := this]; goto $$block3689~b;
  $$block3689~b: call $UpdateOwnersForPeer(p, this); goto $$block3689~a;
  $$block3689~a: assume IsHeap($Heap); goto block3825;
  block3825: stack0o := null; goto true3825to3893, false3825to3842;
  true3825to3893: assume (local4 == stack0o); goto block3893;
  false3825to3842: assume (local4 != stack0o); goto block3842;
  block3893: assert (temp2 != null); goto $$block3893~e;
  $$block3893~e: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block3893~d;
  $$block3893~d: assert (($Heap[temp2, Person.spouse] != null) ==> ($Heap[$Heap[temp2, Person.spouse], Person.spouse] == temp2)); goto $$block3893~c;
  $$block3893~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block3893~b;
  $$block3893~b: $Heap := $Heap[temp2, $inv := Person]; goto $$block3893~a;
  $$block3893~a: assume IsHeap($Heap); goto block3876;
  block3842: goto true3842to3893, false3842to3859;
  true3842to3893: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block3893;
  false3842to3859: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block3859;
  block3859: goto block3876;
  block3876: goto block3740;
  block3740: goto block3995;
  block3995: stack0o := null; goto true3995to4063, false3995to4012;
  true3995to4063: assume (local2 == stack0o); goto block4063;
  false3995to4012: assume (local2 != stack0o); goto block4012;
  block4063: assert (temp0 != null); goto $$block4063~e;
  $$block4063~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block4063~d;
  $$block4063~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block4063~c;
  $$block4063~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block4063~b;
  $$block4063~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block4063~a;
  $$block4063~a: assume IsHeap($Heap); goto block4046;
  block4012: goto true4012to4063, false4012to4029;
  true4012to4063: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block4063;
  false4012to4029: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block4029;
  block4029: goto block4046;
  block4046: goto block3791;
  block3791: return;
  
}

axiom (Microsoft.Contracts.ICheckedException <: System.Object);
axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException);
procedure Person.MarryAssignTheOtherWayAround$Person$notnull(this : ref, p$in : ref where $IsNotNull(p$in, Person));
  requires ($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[p$in, $allocated] == true);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (p$in != this);
  requires ($Heap[this, Person.spouse] == null);
  requires ($Heap[p$in, Person.spouse] == null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[p$in, $ownerRef], $inv] <: $Heap[p$in, $ownerFrame])) || ($Heap[$Heap[p$in, $ownerRef], $localinv] == $BaseClass($Heap[p$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[p$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[p$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[p$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[p$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[p$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[p$in, $ownerFrame]))))) && old(((($o != this) || ($f != Person.spouse)) && (($o != p$in) || ($f != Person.spouse))))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.MarryAssignTheOtherWayAround$Person$notnull(this : ref, p$in : ref) {
  var p : ref where $IsNotNull(p, Person);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~f;
  $$entry~f: assume ($Heap[this, $allocated] == true); goto $$entry~e;
  $$entry~e: p := p$in; goto block5831;
  block5831: goto block6188;
  block6188: temp0 := this; goto $$block6188~g;
  $$block6188~g: assert (temp0 != null); goto $$block6188~f;
  $$block6188~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block6188~e;
  $$block6188~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block6188~d;
  $$block6188~d: havoc temp1; goto $$block6188~c;
  $$block6188~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block6188~b;
  $$block6188~b: assume IsHeap($Heap); goto $$block6188~a;
  $$block6188~a: local2 := null; goto block6205;
  block6205: temp2 := p; goto $$block6205~g;
  $$block6205~g: assert (temp2 != null); goto $$block6205~f;
  $$block6205~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Person)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block6205~e;
  $$block6205~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block6205~d;
  $$block6205~d: havoc temp3; goto $$block6205~c;
  $$block6205~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block6205~b;
  $$block6205~b: assume IsHeap($Heap); goto $$block6205~a;
  $$block6205~a: local4 := null; goto block6222;
  block6222: assert (p != null); goto $$block6222~m;
  $$block6222~m: assert (!($Heap[p, $inv] <: Person) || ($Heap[p, $localinv] == System.Object)); goto $$block6222~l;
  $$block6222~l: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == p)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block6222~k;
  $$block6222~k: assert (((((this == null) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[p, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block6222~j;
  $$block6222~j: $Heap := $Heap[p, Person.spouse := this]; goto $$block6222~i;
  $$block6222~i: call $UpdateOwnersForPeer(p, this); goto $$block6222~h;
  $$block6222~h: assume IsHeap($Heap); goto $$block6222~g;
  $$block6222~g: assert (this != null); goto $$block6222~f;
  $$block6222~f: assert (!($Heap[this, $inv] <: Person) || ($Heap[this, $localinv] == System.Object)); goto $$block6222~e;
  $$block6222~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == this)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block6222~d;
  $$block6222~d: assert (((((p == null) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))))) || ((!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerRef] == $Heap[p, $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[p, $ownerFrame]))); goto $$block6222~c;
  $$block6222~c: $Heap := $Heap[this, Person.spouse := p]; goto $$block6222~b;
  $$block6222~b: call $UpdateOwnersForPeer(this, p); goto $$block6222~a;
  $$block6222~a: assume IsHeap($Heap); goto block6358;
  block6358: stack0o := null; goto true6358to6426, false6358to6375;
  true6358to6426: assume (local4 == stack0o); goto block6426;
  false6358to6375: assume (local4 != stack0o); goto block6375;
  block6426: assert (temp2 != null); goto $$block6426~e;
  $$block6426~e: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block6426~d;
  $$block6426~d: assert (($Heap[temp2, Person.spouse] != null) ==> ($Heap[$Heap[temp2, Person.spouse], Person.spouse] == temp2)); goto $$block6426~c;
  $$block6426~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block6426~b;
  $$block6426~b: $Heap := $Heap[temp2, $inv := Person]; goto $$block6426~a;
  $$block6426~a: assume IsHeap($Heap); goto block6409;
  block6375: goto true6375to6426, false6375to6392;
  true6375to6426: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block6426;
  false6375to6392: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block6392;
  block6392: goto block6409;
  block6409: goto block6273;
  block6273: goto block6528;
  block6528: stack0o := null; goto true6528to6596, false6528to6545;
  true6528to6596: assume (local2 == stack0o); goto block6596;
  false6528to6545: assume (local2 != stack0o); goto block6545;
  block6596: assert (temp0 != null); goto $$block6596~e;
  $$block6596~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block6596~d;
  $$block6596~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block6596~c;
  $$block6596~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block6596~b;
  $$block6596~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block6596~a;
  $$block6596~a: assume IsHeap($Heap); goto block6579;
  block6545: goto true6545to6596, false6545to6562;
  true6545to6596: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block6596;
  false6545to6562: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block6562;
  block6562: goto block6579;
  block6579: goto block6324;
  block6324: return;
  
}

procedure Person.MarryAssignTheOtherWayAround_GoodnessRestored$Person$notnull$System.Boolean(this : ref, p$in : ref where $IsNotNull(p$in, Person), coinFlip$in : bool where true);
  requires ($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[p$in, $allocated] == true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (p$in != this);
  requires ($Heap[this, Person.spouse] == null);
  requires ($Heap[p$in, Person.spouse] == null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[p$in, $ownerRef], $inv] <: $Heap[p$in, $ownerFrame])) || ($Heap[$Heap[p$in, $ownerRef], $localinv] == $BaseClass($Heap[p$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[p$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[p$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[p$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[p$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[p$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[p$in, $ownerFrame]))))) && old(((($o != this) || ($f != Person.spouse)) && (($o != p$in) || ($f != Person.spouse))))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.MarryAssignTheOtherWayAround_GoodnessRestored$Person$notnull$System.Boolean(this : ref, p$in : ref, coinFlip$in : bool) {
  var p : ref where $IsNotNull(p, Person);
  var coinFlip : bool where true;
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~i;
  $$entry~i: assume ($Heap[this, $allocated] == true); goto $$entry~h;
  $$entry~h: p := p$in; goto $$entry~g;
  $$entry~g: coinFlip := coinFlip$in; goto block8415;
  block8415: goto block8772;
  block8772: temp0 := this; goto $$block8772~g;
  $$block8772~g: assert (temp0 != null); goto $$block8772~f;
  $$block8772~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block8772~e;
  $$block8772~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block8772~d;
  $$block8772~d: havoc temp1; goto $$block8772~c;
  $$block8772~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block8772~b;
  $$block8772~b: assume IsHeap($Heap); goto $$block8772~a;
  $$block8772~a: local2 := null; goto block8789;
  block8789: temp2 := p; goto $$block8789~g;
  $$block8789~g: assert (temp2 != null); goto $$block8789~f;
  $$block8789~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Person)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block8789~e;
  $$block8789~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block8789~d;
  $$block8789~d: havoc temp3; goto $$block8789~c;
  $$block8789~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block8789~b;
  $$block8789~b: assume IsHeap($Heap); goto $$block8789~a;
  $$block8789~a: local4 := null; goto block8806;
  block8806: stack0o := p; goto $$block8806~g;
  $$block8806~g: stack1o := this; goto $$block8806~f;
  $$block8806~f: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block8806~e;
  $$block8806~e: assert !$IsImmutable($typeof(stack0o)); goto $$block8806~d;
  $$block8806~d: assert !$IsImmutable($typeof(stack1o)); goto $$block8806~c;
  $$block8806~c: assert ((($Heap[stack1o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack1o, $ownerRef], $inv] <: $Heap[stack1o, $ownerFrame])) || ($Heap[$Heap[stack1o, $ownerRef], $localinv] == $BaseClass($Heap[stack1o, $ownerFrame]))); goto $$block8806~b;
  $$block8806~b: call $SetOwner(stack0o, $Heap[stack1o, $ownerRef], $Heap[stack1o, $ownerFrame]); goto $$block8806~a;
  $$block8806~a: stack0b := coinFlip; goto true8806to8840, false8806to8823;
  true8806to8840: assume !stack0b; goto block8840;
  false8806to8823: assume stack0b; goto block8823;
  block8840: assert (this != null); goto $$block8840~m;
  $$block8840~m: assert (!($Heap[this, $inv] <: Person) || ($Heap[this, $localinv] == System.Object)); goto $$block8840~l;
  $$block8840~l: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == this)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block8840~k;
  $$block8840~k: assert (((((p == null) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))))) || ((!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerRef] == $Heap[p, $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[p, $ownerFrame]))); goto $$block8840~j;
  $$block8840~j: $Heap := $Heap[this, Person.spouse := p]; goto $$block8840~i;
  $$block8840~i: call $UpdateOwnersForPeer(this, p); goto $$block8840~h;
  $$block8840~h: assume IsHeap($Heap); goto $$block8840~g;
  $$block8840~g: assert (p != null); goto $$block8840~f;
  $$block8840~f: assert (!($Heap[p, $inv] <: Person) || ($Heap[p, $localinv] == System.Object)); goto $$block8840~e;
  $$block8840~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == p)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block8840~d;
  $$block8840~d: assert (((((this == null) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[p, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block8840~c;
  $$block8840~c: $Heap := $Heap[p, Person.spouse := this]; goto $$block8840~b;
  $$block8840~b: call $UpdateOwnersForPeer(p, this); goto $$block8840~a;
  $$block8840~a: assume IsHeap($Heap); goto block8857;
  block8823: assert (p != null); goto $$block8823~m;
  $$block8823~m: assert (!($Heap[p, $inv] <: Person) || ($Heap[p, $localinv] == System.Object)); goto $$block8823~l;
  $$block8823~l: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == p)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block8823~k;
  $$block8823~k: assert (((((this == null) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[p, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block8823~j;
  $$block8823~j: $Heap := $Heap[p, Person.spouse := this]; goto $$block8823~i;
  $$block8823~i: call $UpdateOwnersForPeer(p, this); goto $$block8823~h;
  $$block8823~h: assume IsHeap($Heap); goto $$block8823~g;
  $$block8823~g: assert (this != null); goto $$block8823~f;
  $$block8823~f: assert (!($Heap[this, $inv] <: Person) || ($Heap[this, $localinv] == System.Object)); goto $$block8823~e;
  $$block8823~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == this)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block8823~d;
  $$block8823~d: assert (((((p == null) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))))) || ((!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerRef] == $Heap[p, $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[p, $ownerFrame]))); goto $$block8823~c;
  $$block8823~c: $Heap := $Heap[this, Person.spouse := p]; goto $$block8823~b;
  $$block8823~b: call $UpdateOwnersForPeer(this, p); goto $$block8823~a;
  $$block8823~a: assume IsHeap($Heap); goto block8857;
  block8857: goto block8993;
  block8993: stack0o := null; goto true8993to9061, false8993to9010;
  true8993to9061: assume (local4 == stack0o); goto block9061;
  false8993to9010: assume (local4 != stack0o); goto block9010;
  block9061: assert (temp2 != null); goto $$block9061~e;
  $$block9061~e: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block9061~d;
  $$block9061~d: assert (($Heap[temp2, Person.spouse] != null) ==> ($Heap[$Heap[temp2, Person.spouse], Person.spouse] == temp2)); goto $$block9061~c;
  $$block9061~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block9061~b;
  $$block9061~b: $Heap := $Heap[temp2, $inv := Person]; goto $$block9061~a;
  $$block9061~a: assume IsHeap($Heap); goto block9044;
  block9010: goto true9010to9061, false9010to9027;
  true9010to9061: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block9061;
  false9010to9027: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block9027;
  block9027: goto block9044;
  block9044: goto block8908;
  block8908: goto block9163;
  block9163: stack0o := null; goto true9163to9231, false9163to9180;
  true9163to9231: assume (local2 == stack0o); goto block9231;
  false9163to9180: assume (local2 != stack0o); goto block9180;
  block9231: assert (temp0 != null); goto $$block9231~e;
  $$block9231~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block9231~d;
  $$block9231~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block9231~c;
  $$block9231~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block9231~b;
  $$block9231~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block9231~a;
  $$block9231~a: assume IsHeap($Heap); goto block9214;
  block9180: goto true9180to9231, false9180to9197;
  true9180to9231: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block9231;
  false9180to9197: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block9197;
  block9197: goto block9214;
  block9214: goto block8959;
  block8959: return;
  
}

procedure Person.Marry_CaptureThis$Person$notnull(this : ref, p$in : ref where $IsNotNull(p$in, Person));
  requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[p$in, $allocated] == true);
  requires (((($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[p$in, $ownerRef], $inv] <: $Heap[p$in, $ownerFrame])) || ($Heap[$Heap[p$in, $ownerRef], $localinv] == $BaseClass($Heap[p$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[p$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[p$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (p$in != this);
  requires ($Heap[this, Person.spouse] == null);
  requires ($Heap[p$in, Person.spouse] == null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[p$in, $ownerRef], $inv] <: $Heap[p$in, $ownerFrame])) || ($Heap[$Heap[p$in, $ownerRef], $localinv] == $BaseClass($Heap[p$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[p$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[p$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[this, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[this, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame]))))) && old(((($o != this) || ($f != Person.spouse)) && (($o != p$in) || ($f != Person.spouse))))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.Marry_CaptureThis$Person$notnull(this : ref, p$in : ref) {
  var p : ref where $IsNotNull(p, Person);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~k;
  $$entry~k: assume ($Heap[this, $allocated] == true); goto $$entry~j;
  $$entry~j: p := p$in; goto block11135;
  block11135: goto block11492;
  block11492: temp0 := this; goto $$block11492~g;
  $$block11492~g: assert (temp0 != null); goto $$block11492~f;
  $$block11492~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block11492~e;
  $$block11492~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block11492~d;
  $$block11492~d: havoc temp1; goto $$block11492~c;
  $$block11492~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block11492~b;
  $$block11492~b: assume IsHeap($Heap); goto $$block11492~a;
  $$block11492~a: local2 := null; goto block11509;
  block11509: temp2 := p; goto $$block11509~g;
  $$block11509~g: assert (temp2 != null); goto $$block11509~f;
  $$block11509~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Person)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block11509~e;
  $$block11509~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block11509~d;
  $$block11509~d: havoc temp3; goto $$block11509~c;
  $$block11509~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block11509~b;
  $$block11509~b: assume IsHeap($Heap); goto $$block11509~a;
  $$block11509~a: local4 := null; goto block11526;
  block11526: assert (p != null); goto $$block11526~m;
  $$block11526~m: assert (!($Heap[p, $inv] <: Person) || ($Heap[p, $localinv] == System.Object)); goto $$block11526~l;
  $$block11526~l: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == p)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block11526~k;
  $$block11526~k: assert (((((this == null) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[p, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block11526~j;
  $$block11526~j: $Heap := $Heap[p, Person.spouse := this]; goto $$block11526~i;
  $$block11526~i: call $UpdateOwnersForPeer(p, this); goto $$block11526~h;
  $$block11526~h: assume IsHeap($Heap); goto $$block11526~g;
  $$block11526~g: assert (this != null); goto $$block11526~f;
  $$block11526~f: assert (!($Heap[this, $inv] <: Person) || ($Heap[this, $localinv] == System.Object)); goto $$block11526~e;
  $$block11526~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == this)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block11526~d;
  $$block11526~d: assert (((((p == null) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))))) || ((!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerRef] == $Heap[p, $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[p, $ownerFrame]))); goto $$block11526~c;
  $$block11526~c: $Heap := $Heap[this, Person.spouse := p]; goto $$block11526~b;
  $$block11526~b: call $UpdateOwnersForPeer(this, p); goto $$block11526~a;
  $$block11526~a: assume IsHeap($Heap); goto block11662;
  block11662: stack0o := null; goto true11662to11730, false11662to11679;
  true11662to11730: assume (local4 == stack0o); goto block11730;
  false11662to11679: assume (local4 != stack0o); goto block11679;
  block11730: assert (temp2 != null); goto $$block11730~e;
  $$block11730~e: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block11730~d;
  $$block11730~d: assert (($Heap[temp2, Person.spouse] != null) ==> ($Heap[$Heap[temp2, Person.spouse], Person.spouse] == temp2)); goto $$block11730~c;
  $$block11730~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block11730~b;
  $$block11730~b: $Heap := $Heap[temp2, $inv := Person]; goto $$block11730~a;
  $$block11730~a: assume IsHeap($Heap); goto block11713;
  block11679: goto true11679to11730, false11679to11696;
  true11679to11730: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block11730;
  false11679to11696: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block11696;
  block11696: goto block11713;
  block11713: goto block11577;
  block11577: goto block11832;
  block11832: stack0o := null; goto true11832to11900, false11832to11849;
  true11832to11900: assume (local2 == stack0o); goto block11900;
  false11832to11849: assume (local2 != stack0o); goto block11849;
  block11900: assert (temp0 != null); goto $$block11900~e;
  $$block11900~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block11900~d;
  $$block11900~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block11900~c;
  $$block11900~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block11900~b;
  $$block11900~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block11900~a;
  $$block11900~a: assume IsHeap($Heap); goto block11883;
  block11849: goto true11849to11900, false11849to11866;
  true11849to11900: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block11900;
  false11849to11866: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block11866;
  block11866: goto block11883;
  block11883: goto block11628;
  block11628: return;
  
}

procedure Person.Marry_CaptureEither$Person$notnull(this : ref, p$in : ref where $IsNotNull(p$in, Person));
  requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder);
  requires ($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[p$in, $allocated] == true);
  requires (p$in != this);
  requires ($Heap[this, Person.spouse] == null);
  requires ($Heap[p$in, Person.spouse] == null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[p$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[p$in, $ownerRef], $inv] <: $Heap[p$in, $ownerFrame])) || ($Heap[$Heap[p$in, $ownerRef], $localinv] == $BaseClass($Heap[p$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[p$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[p$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[this, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[this, $ownerFrame]))) && ((old($Heap)[$o, $ownerRef] != old($Heap)[p$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[p$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && (old((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame]))) || old((($Heap[$o, $ownerRef] == $Heap[p$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[p$in, $ownerFrame])))))) && old(((($o != this) || ($f != Person.spouse)) && (($o != p$in) || ($f != Person.spouse))))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.Marry_CaptureEither$Person$notnull(this : ref, p$in : ref) {
  var p : ref where $IsNotNull(p, Person);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~m;
  $$entry~m: assume ($Heap[this, $allocated] == true); goto $$entry~l;
  $$entry~l: p := p$in; goto block13617;
  block13617: goto block13923;
  block13923: temp0 := this; goto $$block13923~g;
  $$block13923~g: assert (temp0 != null); goto $$block13923~f;
  $$block13923~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block13923~e;
  $$block13923~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block13923~d;
  $$block13923~d: havoc temp1; goto $$block13923~c;
  $$block13923~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block13923~b;
  $$block13923~b: assume IsHeap($Heap); goto $$block13923~a;
  $$block13923~a: local2 := null; goto block13940;
  block13940: temp2 := p; goto $$block13940~g;
  $$block13940~g: assert (temp2 != null); goto $$block13940~f;
  $$block13940~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Person)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block13940~e;
  $$block13940~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block13940~d;
  $$block13940~d: havoc temp3; goto $$block13940~c;
  $$block13940~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block13940~b;
  $$block13940~b: assume IsHeap($Heap); goto $$block13940~a;
  $$block13940~a: local4 := null; goto block13957;
  block13957: assert (this != null); goto $$block13957~m;
  $$block13957~m: assert (!($Heap[this, $inv] <: Person) || ($Heap[this, $localinv] == System.Object)); goto $$block13957~l;
  $$block13957~l: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == this)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block13957~k;
  $$block13957~k: assert (((((p == null) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))))) || ((!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[p, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[this, $ownerRef] == $Heap[p, $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[p, $ownerFrame]))); goto $$block13957~j;
  $$block13957~j: $Heap := $Heap[this, Person.spouse := p]; goto $$block13957~i;
  $$block13957~i: call $UpdateOwnersForPeer(this, p); goto $$block13957~h;
  $$block13957~h: assume IsHeap($Heap); goto $$block13957~g;
  $$block13957~g: assert (p != null); goto $$block13957~f;
  $$block13957~f: assert (!($Heap[p, $inv] <: Person) || ($Heap[p, $localinv] == System.Object)); goto $$block13957~e;
  $$block13957~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Person)) && ($Heap[$o, Person.spouse] == p)) ==> (!($Heap[$o, $inv] <: Person) || ($Heap[$o, $localinv] == System.Object)))); goto $$block13957~d;
  $$block13957~d: assert (((((this == null) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[p, $ownerRef], $inv] <: $Heap[p, $ownerFrame]) || ($Heap[$Heap[p, $ownerRef], $localinv] == $BaseClass($Heap[p, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[p, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[p, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block13957~c;
  $$block13957~c: $Heap := $Heap[p, Person.spouse := this]; goto $$block13957~b;
  $$block13957~b: call $UpdateOwnersForPeer(p, this); goto $$block13957~a;
  $$block13957~a: assume IsHeap($Heap); goto block14093;
  block14093: stack0o := null; goto true14093to14161, false14093to14110;
  true14093to14161: assume (local4 == stack0o); goto block14161;
  false14093to14110: assume (local4 != stack0o); goto block14110;
  block14161: assert (temp2 != null); goto $$block14161~e;
  $$block14161~e: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block14161~d;
  $$block14161~d: assert (($Heap[temp2, Person.spouse] != null) ==> ($Heap[$Heap[temp2, Person.spouse], Person.spouse] == temp2)); goto $$block14161~c;
  $$block14161~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block14161~b;
  $$block14161~b: $Heap := $Heap[temp2, $inv := Person]; goto $$block14161~a;
  $$block14161~a: assume IsHeap($Heap); goto block14144;
  block14110: goto true14110to14161, false14110to14127;
  true14110to14161: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block14161;
  false14110to14127: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block14127;
  block14127: goto block14144;
  block14144: goto block14008;
  block14008: goto block14263;
  block14263: stack0o := null; goto true14263to14331, false14263to14280;
  true14263to14331: assume (local2 == stack0o); goto block14331;
  false14263to14280: assume (local2 != stack0o); goto block14280;
  block14331: assert (temp0 != null); goto $$block14331~e;
  $$block14331~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block14331~d;
  $$block14331~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block14331~c;
  $$block14331~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block14331~b;
  $$block14331~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block14331~a;
  $$block14331~a: assume IsHeap($Heap); goto block14314;
  block14280: goto true14280to14331, false14280to14297;
  true14280to14331: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block14331;
  false14280to14297: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block14297;
  block14297: goto block14314;
  block14314: goto block14059;
  block14059: return;
  
}

procedure Person.MM(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.MM(this : ref) {
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~n;
  $$entry~n: assume ($Heap[this, $allocated] == true); goto block15827;
  block15827: goto block15929;
  block15929: assert (this != null); goto $$block15929~b;
  $$block15929~b: stack0o := $Heap[this, Person.spouse]; goto $$block15929~a;
  $$block15929~a: stack1o := null; goto true15929to16048, false15929to15946;
  true15929to16048: assume (stack0o == stack1o); goto block16048;
  false15929to15946: assume (stack0o != stack1o); goto block15946;
  block16048: return;
  block15946: assert (($Heap[this, $ownerRef] == $Heap[$Heap[this, Person.spouse], $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[$Heap[this, Person.spouse], $ownerFrame])); goto block16031;
  block16031: goto block16048;
  
}

axiom (System.String <: System.String);
axiom ($BaseClass(System.String) == System.Object);
axiom ((System.String <: $BaseClass(System.String)) && (AsDirectSubClass(System.String, $BaseClass(System.String)) == System.String));
axiom ($IsImmutable(System.String) && ($AsImmutable(System.String) == System.String));
axiom (System.IComparable <: System.Object);
axiom $IsMemberlessType(System.IComparable);
axiom (System.String <: System.IComparable);
axiom (System.ICloneable <: System.Object);
axiom $IsMemberlessType(System.ICloneable);
axiom (System.String <: System.ICloneable);
axiom (System.IConvertible <: System.Object);
axiom $IsMemberlessType(System.IConvertible);
axiom (System.String <: System.IConvertible);
axiom (System.IComparable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IComparable`1...System.String);
axiom (System.String <: System.IComparable`1...System.String);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Object);
axiom (System.Collections.IEnumerable <: System.Object);
axiom $IsMemberlessType(System.Collections.IEnumerable);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Collections.IEnumerable);
axiom $IsMemberlessType(System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.IEnumerable);
axiom (System.IEquatable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IEquatable`1...System.String);
axiom (System.String <: System.IEquatable`1...System.String);
axiom (forall $U : name :: {($U <: System.String)} (($U <: System.String) ==> ($U == System.String)));
procedure Person.NN(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.NN(this : ref) {
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~o;
  $$entry~o: assume ($Heap[this, $allocated] == true); goto block16915;
  block16915: goto block17017;
  block17017: assert (this != null); goto $$block17017~b;
  $$block17017~b: stack0o := $Heap[this, Person.possn]; goto $$block17017~a;
  $$block17017~a: stack1o := null; goto true17017to17136, false17017to17034;
  true17017to17136: assume (stack0o == stack1o); goto block17136;
  false17017to17034: assume (stack0o != stack1o); goto block17034;
  block17136: return;
  block17034: assert (($Heap[$Heap[this, Person.possn], $ownerRef] == this) && ($Heap[$Heap[this, Person.possn], $ownerFrame] == TypeName(TypeObject(Person)))); goto block17119;
  block17119: goto block17136;
  
}

axiom (Possession <: Possession);
axiom ($BaseClass(Possession) == System.Object);
axiom ((Possession <: $BaseClass(Possession)) && (AsDirectSubClass(Possession, $BaseClass(Possession)) == Possession));
axiom (!$IsImmutable(Possession) && ($AsMutable(Possession) == Possession));
axiom (System.Type <: System.Type);
axiom (System.Reflection.MemberInfo <: System.Reflection.MemberInfo);
axiom ($BaseClass(System.Reflection.MemberInfo) == System.Object);
axiom ((System.Reflection.MemberInfo <: $BaseClass(System.Reflection.MemberInfo)) && (AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo));
axiom ($IsImmutable(System.Reflection.MemberInfo) && ($AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo));
axiom (System.Reflection.ICustomAttributeProvider <: System.Object);
axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider);
axiom (System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider);
axiom (System.Runtime.InteropServices._MemberInfo <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo);
axiom (System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo);
axiom $IsMemberlessType(System.Reflection.MemberInfo);
axiom ($BaseClass(System.Type) == System.Reflection.MemberInfo);
axiom ((System.Type <: $BaseClass(System.Type)) && (AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type));
axiom ($IsImmutable(System.Type) && ($AsImmutable(System.Type) == System.Type));
axiom (System.Runtime.InteropServices._Type <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Type);
axiom (System.Type <: System.Runtime.InteropServices._Type);
axiom (System.Reflection.IReflect <: System.Object);
axiom $IsMemberlessType(System.Reflection.IReflect);
axiom (System.Type <: System.Reflection.IReflect);
axiom $IsMemberlessType(System.Type);
procedure Person.PP(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.PP(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var stack50000o : ref;
  var stack0o : ref;
  var o : ref where $Is(o, System.Object);
  var stack1o : ref;
  var stack2s : struct;
  var stack2o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~p;
  $$entry~p: assume ($Heap[this, $allocated] == true); goto block17935;
  block17935: goto block18088;
  block18088: temp0 := this; goto $$block18088~g;
  $$block18088~g: assert (temp0 != null); goto $$block18088~f;
  $$block18088~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block18088~e;
  $$block18088~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block18088~d;
  $$block18088~d: havoc temp1; goto $$block18088~c;
  $$block18088~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block18088~b;
  $$block18088~b: assume IsHeap($Heap); goto $$block18088~a;
  $$block18088~a: local2 := null; goto block18105;
  block18105: havoc stack50000o; goto $$block18105~t;
  $$block18105~t: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == System.Object)); goto $$block18105~s;
  $$block18105~s: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block18105~r;
  $$block18105~r: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block18105~q;
  $$block18105~q: assert (stack50000o != null); goto $$block18105~p;
  $$block18105~p: call System.Object..ctor(stack50000o); goto $$block18105~o;
  $$block18105~o: stack0o := stack50000o; goto $$block18105~n;
  $$block18105~n: o := stack0o; goto $$block18105~m;
  $$block18105~m: stack0o := o; goto $$block18105~l;
  $$block18105~l: assert (stack0o != null); goto $$block18105~k;
  $$block18105~k: stack0o := stack0o; goto $$block18105~j;
  $$block18105~j: stack1o := this; goto $$block18105~i;
  $$block18105~i: havoc stack2s; goto $$block18105~h;
  $$block18105~h: assume $IsTokenForType(stack2s, Person); goto $$block18105~g;
  $$block18105~g: stack2o := TypeObject(Person); goto $$block18105~f;
  $$block18105~f: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block18105~e;
  $$block18105~e: assert !$IsImmutable($typeof(stack0o)); goto $$block18105~d;
  $$block18105~d: assert ($typeof(stack1o) <: TypeName(stack2o)); goto $$block18105~c;
  $$block18105~c: assert !($Heap[stack1o, $inv] <: TypeName(stack2o)); goto $$block18105~b;
  $$block18105~b: call $SetOwner(stack0o, stack1o, TypeName(stack2o)); goto $$block18105~a;
  $$block18105~a: assert (($Heap[o, $ownerRef] == this) && ($Heap[o, $ownerFrame] == TypeName(TypeObject(Person)))); goto block18190;
  block18190: goto block18275;
  block18275: stack0o := null; goto true18275to18343, false18275to18292;
  true18275to18343: assume (local2 == stack0o); goto block18343;
  false18275to18292: assume (local2 != stack0o); goto block18292;
  block18343: assert (temp0 != null); goto $$block18343~e;
  $$block18343~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block18343~d;
  $$block18343~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block18343~c;
  $$block18343~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block18343~b;
  $$block18343~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block18343~a;
  $$block18343~a: assume IsHeap($Heap); goto block18326;
  block18292: goto true18292to18343, false18292to18309;
  true18292to18343: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block18343;
  false18292to18309: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block18309;
  block18309: goto block18326;
  block18326: goto block18241;
  block18241: return;
  
}

procedure System.Object..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(System.Object <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure Person.A0$System.Object$notnull(this : ref, subject$in : ref where $IsNotNull(subject$in, System.Object));
  free requires ($Heap[subject$in, $allocated] == true);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[subject$in, $ownerRef], $inv] <: $Heap[subject$in, $ownerFrame])) || ($Heap[$Heap[subject$in, $ownerRef], $localinv] == $BaseClass($Heap[subject$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[subject$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[subject$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.A0$System.Object$notnull(this : ref, subject$in : ref) {
  var subject : ref where $IsNotNull(subject, System.Object);
  var stack0o : ref;
  var stack1o : ref;
  var stack2s : struct;
  var stack2o : ref;
  entry: assume $IsNotNull(this, Person); goto $$entry~r;
  $$entry~r: assume ($Heap[this, $allocated] == true); goto $$entry~q;
  $$entry~q: subject := subject$in; goto block19278;
  block19278: goto block19380;
  block19380: stack0o := subject; goto $$block19380~i;
  $$block19380~i: stack1o := this; goto $$block19380~h;
  $$block19380~h: havoc stack2s; goto $$block19380~g;
  $$block19380~g: assume $IsTokenForType(stack2s, Person); goto $$block19380~f;
  $$block19380~f: stack2o := TypeObject(Person); goto $$block19380~e;
  $$block19380~e: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block19380~d;
  $$block19380~d: assert !$IsImmutable($typeof(stack0o)); goto $$block19380~c;
  $$block19380~c: assert ($typeof(stack1o) <: TypeName(stack2o)); goto $$block19380~b;
  $$block19380~b: assert !($Heap[stack1o, $inv] <: TypeName(stack2o)); goto $$block19380~a;
  $$block19380~a: call $SetOwner(stack0o, stack1o, TypeName(stack2o)); return;
  
}

procedure Person.A1$Possession$notnull(this : ref, subject$in : ref where $IsNotNull(subject$in, Possession));
  requires ($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[subject$in, $allocated] == true);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[subject$in, $ownerRef], $inv] <: $Heap[subject$in, $ownerFrame])) || ($Heap[$Heap[subject$in, $ownerRef], $localinv] == $BaseClass($Heap[subject$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[subject$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[subject$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[subject$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[subject$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[subject$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[subject$in, $ownerFrame]))))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.A1$Possession$notnull(this : ref, subject$in : ref) {
  var subject : ref where $IsNotNull(subject, Possession);
  var stack0o : ref;
  var stack1o : ref;
  var stack2s : struct;
  var stack2o : ref;
  entry: assume $IsNotNull(this, Person); goto $$entry~t;
  $$entry~t: assume ($Heap[this, $allocated] == true); goto $$entry~s;
  $$entry~s: subject := subject$in; goto block19754;
  block19754: goto block19856;
  block19856: stack0o := subject; goto $$block19856~i;
  $$block19856~i: stack1o := this; goto $$block19856~h;
  $$block19856~h: havoc stack2s; goto $$block19856~g;
  $$block19856~g: assume $IsTokenForType(stack2s, System.String); goto $$block19856~f;
  $$block19856~f: stack2o := TypeObject(System.String); goto $$block19856~e;
  $$block19856~e: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block19856~d;
  $$block19856~d: assert !$IsImmutable($typeof(stack0o)); goto $$block19856~c;
  $$block19856~c: assert ($typeof(stack1o) <: TypeName(stack2o)); goto $$block19856~b;
  $$block19856~b: assert !($Heap[stack1o, $inv] <: TypeName(stack2o)); goto $$block19856~a;
  $$block19856~a: call $SetOwner(stack0o, stack1o, TypeName(stack2o)); return;
  
}

procedure Person.A2$Possession$notnull(this : ref, subject$in : ref where $IsNotNull(subject$in, Possession));
  requires ($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[subject$in, $allocated] == true);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[subject$in, $ownerRef], $inv] <: $Heap[subject$in, $ownerFrame])) || ($Heap[$Heap[subject$in, $ownerRef], $localinv] == $BaseClass($Heap[subject$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[subject$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[subject$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[subject$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[subject$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[subject$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[subject$in, $ownerFrame]))))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.A2$Possession$notnull(this : ref, subject$in : ref) {
  var subject : ref where $IsNotNull(subject, Possession);
  var stack0o : ref;
  var stack1o : ref;
  var stack2s : struct;
  var stack2o : ref;
  entry: assume $IsNotNull(this, Person); goto $$entry~v;
  $$entry~v: assume ($Heap[this, $allocated] == true); goto $$entry~u;
  $$entry~u: subject := subject$in; goto block20230;
  block20230: goto block20332;
  block20332: stack0o := subject; goto $$block20332~i;
  $$block20332~i: stack1o := this; goto $$block20332~h;
  $$block20332~h: havoc stack2s; goto $$block20332~g;
  $$block20332~g: assume $IsTokenForType(stack2s, Person); goto $$block20332~f;
  $$block20332~f: stack2o := TypeObject(Person); goto $$block20332~e;
  $$block20332~e: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block20332~d;
  $$block20332~d: assert !$IsImmutable($typeof(stack0o)); goto $$block20332~c;
  $$block20332~c: assert ($typeof(stack1o) <: TypeName(stack2o)); goto $$block20332~b;
  $$block20332~b: assert !($Heap[stack1o, $inv] <: TypeName(stack2o)); goto $$block20332~a;
  $$block20332~a: call $SetOwner(stack0o, stack1o, TypeName(stack2o)); return;
  
}

procedure Person.A3$Possession$notnull(this : ref, subject$in : ref where $IsNotNull(subject$in, Possession));
  requires ($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[subject$in, $allocated] == true);
  requires ((((($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[subject$in, $ownerRef], $inv] <: $Heap[subject$in, $ownerFrame])) || ($Heap[$Heap[subject$in, $ownerRef], $localinv] == $BaseClass($Heap[subject$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[subject$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[subject$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc)))))) && !(($Heap[this, $ownerRef] == $Heap[subject$in, $ownerRef]) && ($Heap[this, $ownerFrame] == $Heap[subject$in, $ownerFrame])));
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[subject$in, $ownerRef], $inv] <: $Heap[subject$in, $ownerFrame])) || ($Heap[$Heap[subject$in, $ownerRef], $localinv] == $BaseClass($Heap[subject$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[subject$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[subject$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[subject$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[subject$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[subject$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[subject$in, $ownerFrame]))))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.A3$Possession$notnull(this : ref, subject$in : ref) {
  var subject : ref where $IsNotNull(subject, Possession);
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var stack0o : ref;
  var stack1o : ref;
  var stack2s : struct;
  var stack2o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Person); goto $$entry~x;
  $$entry~x: assume ($Heap[this, $allocated] == true); goto $$entry~w;
  $$entry~w: subject := subject$in; goto block21012;
  block21012: goto block21233;
  block21233: temp0 := this; goto $$block21233~g;
  $$block21233~g: assert (temp0 != null); goto $$block21233~f;
  $$block21233~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block21233~e;
  $$block21233~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block21233~d;
  $$block21233~d: havoc temp1; goto $$block21233~c;
  $$block21233~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block21233~b;
  $$block21233~b: assume IsHeap($Heap); goto $$block21233~a;
  $$block21233~a: local2 := null; goto block21250;
  block21250: stack0o := subject; goto $$block21250~i;
  $$block21250~i: stack1o := this; goto $$block21250~h;
  $$block21250~h: havoc stack2s; goto $$block21250~g;
  $$block21250~g: assume $IsTokenForType(stack2s, Person); goto $$block21250~f;
  $$block21250~f: stack2o := TypeObject(Person); goto $$block21250~e;
  $$block21250~e: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block21250~d;
  $$block21250~d: assert !$IsImmutable($typeof(stack0o)); goto $$block21250~c;
  $$block21250~c: assert ($typeof(stack1o) <: TypeName(stack2o)); goto $$block21250~b;
  $$block21250~b: assert !($Heap[stack1o, $inv] <: TypeName(stack2o)); goto $$block21250~a;
  $$block21250~a: call $SetOwner(stack0o, stack1o, TypeName(stack2o)); goto block21335;
  block21335: stack0o := null; goto true21335to21403, false21335to21352;
  true21335to21403: assume (local2 == stack0o); goto block21403;
  false21335to21352: assume (local2 != stack0o); goto block21352;
  block21403: assert (temp0 != null); goto $$block21403~e;
  $$block21403~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block21403~d;
  $$block21403~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block21403~c;
  $$block21403~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block21403~b;
  $$block21403~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block21403~a;
  $$block21403~a: assume IsHeap($Heap); goto block21386;
  block21352: goto true21352to21403, false21352to21369;
  true21352to21403: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block21403;
  false21352to21369: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block21369;
  block21369: goto block21386;
  block21386: goto block21301;
  block21301: return;
  
}

procedure Person.B0$System.Object$notnull(this : ref, subject$in : ref where $IsNotNull(subject$in, System.Object));
  free requires ($Heap[subject$in, $allocated] == true);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[subject$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[subject$in, $ownerRef], $inv] <: $Heap[subject$in, $ownerFrame])) || ($Heap[$Heap[subject$in, $ownerRef], $localinv] == $BaseClass($Heap[subject$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[subject$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[subject$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.B0$System.Object$notnull(this : ref, subject$in : ref) {
  var subject : ref where $IsNotNull(subject, System.Object);
  var stack0o : ref;
  var stack1o : ref;
  entry: assume $IsNotNull(this, Person); goto $$entry~z;
  $$entry~z: assume ($Heap[this, $allocated] == true); goto $$entry~y;
  $$entry~y: subject := subject$in; goto block22270;
  block22270: goto block22372;
  block22372: stack0o := subject; goto $$block22372~g;
  $$block22372~g: stack1o := this; goto $$block22372~f;
  $$block22372~f: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block22372~e;
  $$block22372~e: assert !$IsImmutable($typeof(stack0o)); goto $$block22372~d;
  $$block22372~d: assert !$IsImmutable($typeof(stack1o)); goto $$block22372~c;
  $$block22372~c: assert ((($Heap[stack1o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack1o, $ownerRef], $inv] <: $Heap[stack1o, $ownerFrame])) || ($Heap[$Heap[stack1o, $ownerRef], $localinv] == $BaseClass($Heap[stack1o, $ownerFrame]))); goto $$block22372~b;
  $$block22372~b: call $SetOwner(stack0o, $Heap[stack1o, $ownerRef], $Heap[stack1o, $ownerFrame]); goto $$block22372~a;
  $$block22372~a: assume false; return;
  
}

procedure Person.B1(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.B1(this : ref) {
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  var stack50000o : ref;
  var subject : ref where $Is(subject, System.Object);
  entry: assume $IsNotNull(this, Person); goto $$entry~aa;
  $$entry~aa: assume ($Heap[this, $allocated] == true); goto block22933;
  block22933: goto block23035;
  block23035: assert (this != null); goto $$block23035~b;
  $$block23035~b: stack0o := $Heap[this, Person.possn]; goto $$block23035~a;
  $$block23035~a: stack1o := null; goto true23035to23069, false23035to23052;
  true23035to23069: assume (stack0o == stack1o); goto block23069;
  false23035to23052: assume (stack0o != stack1o); goto block23052;
  block23069: return;
  block23052: havoc stack50000o; goto $$block23052~s;
  $$block23052~s: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == System.Object)); goto $$block23052~r;
  $$block23052~r: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block23052~q;
  $$block23052~q: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block23052~p;
  $$block23052~p: assert (stack50000o != null); goto $$block23052~o;
  $$block23052~o: call System.Object..ctor(stack50000o); goto $$block23052~n;
  $$block23052~n: stack0o := stack50000o; goto $$block23052~m;
  $$block23052~m: subject := stack0o; goto $$block23052~l;
  $$block23052~l: stack0o := subject; goto $$block23052~k;
  $$block23052~k: assert (stack0o != null); goto $$block23052~j;
  $$block23052~j: stack0o := stack0o; goto $$block23052~i;
  $$block23052~i: assert (this != null); goto $$block23052~h;
  $$block23052~h: stack1o := $Heap[this, Person.possn]; goto $$block23052~g;
  $$block23052~g: assert (stack1o != null); goto $$block23052~f;
  $$block23052~f: stack1o := stack1o; goto $$block23052~e;
  $$block23052~e: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block23052~d;
  $$block23052~d: assert !$IsImmutable($typeof(stack0o)); goto $$block23052~c;
  $$block23052~c: assert !$IsImmutable($typeof(stack1o)); goto $$block23052~b;
  $$block23052~b: assert ((($Heap[stack1o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack1o, $ownerRef], $inv] <: $Heap[stack1o, $ownerFrame])) || ($Heap[$Heap[stack1o, $ownerRef], $localinv] == $BaseClass($Heap[stack1o, $ownerFrame]))); goto $$block23052~a;
  $$block23052~a: call $SetOwner(stack0o, $Heap[stack1o, $ownerRef], $Heap[stack1o, $ownerFrame]); goto block23069;
  
}

procedure Person.B2(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person.B2(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  var stack50000o : ref;
  var subject : ref where $Is(subject, System.Object);
  entry: assume $IsNotNull(this, Person); goto $$entry~ab;
  $$entry~ab: assume ($Heap[this, $allocated] == true); goto block23851;
  block23851: goto block24004;
  block24004: temp0 := this; goto $$block24004~g;
  $$block24004~g: assert (temp0 != null); goto $$block24004~f;
  $$block24004~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Person)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block24004~e;
  $$block24004~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block24004~d;
  $$block24004~d: havoc temp1; goto $$block24004~c;
  $$block24004~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block24004~b;
  $$block24004~b: assume IsHeap($Heap); goto $$block24004~a;
  $$block24004~a: local2 := null; goto block24021;
  block24021: assert (this != null); goto $$block24021~b;
  $$block24021~b: stack0o := $Heap[this, Person.possn]; goto $$block24021~a;
  $$block24021~a: stack1o := null; goto true24021to24055, false24021to24038;
  true24021to24055: assume (stack0o == stack1o); goto block24055;
  false24021to24038: assume (stack0o != stack1o); goto block24038;
  block24055: goto block24140;
  block24038: havoc stack50000o; goto $$block24038~s;
  $$block24038~s: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == System.Object)); goto $$block24038~r;
  $$block24038~r: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block24038~q;
  $$block24038~q: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block24038~p;
  $$block24038~p: assert (stack50000o != null); goto $$block24038~o;
  $$block24038~o: call System.Object..ctor(stack50000o); goto $$block24038~n;
  $$block24038~n: stack0o := stack50000o; goto $$block24038~m;
  $$block24038~m: subject := stack0o; goto $$block24038~l;
  $$block24038~l: stack0o := subject; goto $$block24038~k;
  $$block24038~k: assert (stack0o != null); goto $$block24038~j;
  $$block24038~j: stack0o := stack0o; goto $$block24038~i;
  $$block24038~i: assert (this != null); goto $$block24038~h;
  $$block24038~h: stack1o := $Heap[this, Person.possn]; goto $$block24038~g;
  $$block24038~g: assert (stack1o != null); goto $$block24038~f;
  $$block24038~f: stack1o := stack1o; goto $$block24038~e;
  $$block24038~e: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block24038~d;
  $$block24038~d: assert !$IsImmutable($typeof(stack0o)); goto $$block24038~c;
  $$block24038~c: assert !$IsImmutable($typeof(stack1o)); goto $$block24038~b;
  $$block24038~b: assert ((($Heap[stack1o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack1o, $ownerRef], $inv] <: $Heap[stack1o, $ownerFrame])) || ($Heap[$Heap[stack1o, $ownerRef], $localinv] == $BaseClass($Heap[stack1o, $ownerFrame]))); goto $$block24038~a;
  $$block24038~a: call $SetOwner(stack0o, $Heap[stack1o, $ownerRef], $Heap[stack1o, $ownerFrame]); goto block24055;
  block24140: stack0o := null; goto true24140to24208, false24140to24157;
  true24140to24208: assume (local2 == stack0o); goto block24208;
  false24140to24157: assume (local2 != stack0o); goto block24157;
  block24208: assert (temp0 != null); goto $$block24208~e;
  $$block24208~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block24208~d;
  $$block24208~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block24208~c;
  $$block24208~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block24208~b;
  $$block24208~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block24208~a;
  $$block24208~a: assume IsHeap($Heap); goto block24191;
  block24157: goto true24157to24208, false24157to24174;
  true24157to24208: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block24208;
  false24157to24174: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block24174;
  block24174: goto block24191;
  block24191: goto block24106;
  block24106: return;
  
}

procedure Person..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Person)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Person <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation Person..ctor(this : ref) {
  var temp0 : ref;
  entry: assume $IsNotNull(this, Person); goto $$entry~af;
  $$entry~af: assume ($Heap[this, $allocated] == true); goto $$entry~ae;
  $$entry~ae: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~ad;
  $$entry~ad: assume ($Heap[this, Person.possn] == null); goto $$entry~ac;
  $$entry~ac: assume ($Heap[this, Person.spouse] == null); goto block25092;
  block25092: goto block25109;
  block25109: assert (this != null); goto $$block25109~a;
  $$block25109~a: call System.Object..ctor(this); goto block25177;
  block25177: temp0 := this; goto $$block25177~f;
  $$block25177~f: assert (temp0 != null); goto $$block25177~e;
  $$block25177~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block25177~d;
  $$block25177~d: assert (($Heap[temp0, Person.spouse] != null) ==> ($Heap[$Heap[temp0, Person.spouse], Person.spouse] == temp0)); goto $$block25177~c;
  $$block25177~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Person)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block25177~b;
  $$block25177~b: $Heap := $Heap[temp0, $inv := Person]; goto $$block25177~a;
  $$block25177~a: assume IsHeap($Heap); return;
  
}

procedure Person..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Person..cctor() {
  entry: goto block25466;
  block25466: goto block25517;
  block25517: return;
  
}

procedure Possession..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Possession)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Possession <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation Possession..ctor(this : ref) {
  entry: assume $IsNotNull(this, Possession); goto $$entry~ah;
  $$entry~ah: assume ($Heap[this, $allocated] == true); goto $$entry~ag;
  $$entry~ag: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto block25721;
  block25721: goto block25738;
  block25738: assert (this != null); goto $$block25738~f;
  $$block25738~f: call System.Object..ctor(this); goto $$block25738~e;
  $$block25738~e: assert (this != null); goto $$block25738~d;
  $$block25738~d: assert (($Heap[this, $inv] == System.Object) && ($Heap[this, $localinv] == $typeof(this))); goto $$block25738~c;
  $$block25738~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == this)) && ($Heap[$p, $ownerFrame] == Possession)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block25738~b;
  $$block25738~b: $Heap := $Heap[this, $inv := Possession]; goto $$block25738~a;
  $$block25738~a: assume IsHeap($Heap); return;
  
}

